/LMAR=0/XLINE=3/FONT#0=BASL30/FONT#1=BASI30/FONT#2=BASB30/FONT#10=BAXM30/FONT#11=ZERO30/FONT#3=STA200/FONT#4=NGB25
␈↓ ↓H␈↓␈↓βS␈↓∧ Department of Computer Science, STANFORD UNIVERSITY, Stanford, California 94305

␈↓ ↓H␈↓∧Telephone 415 497-4430␈↓ 	TDecember 22, 1980 




␈↓ ↓H␈↓Professor W. W. Bledsoe
␈↓ ↓H␈↓Department of Mathematics
␈↓ ↓H␈↓University of Texas
␈↓ ↓H␈↓Austin, Texas 78712

␈↓ ↓H␈↓Dear Woody:

␈↓ ↓H␈↓        I␈αhope␈αto␈αmake␈αthe␈αmeeting␈αin␈αSF,␈αpossibly␈α
a␈αbit␈αlate␈αbecause␈αof␈αa␈αclass.␈α Anyway␈αI␈αhave␈α
an
␈↓ ↓H␈↓idea for an intermediate prize.

␈↓ ↓H␈↓        The␈α∞program␈α∞used␈α∞to␈α∂verify␈α∞the␈α∞four-color␈α∞theorem␈α∞was␈α∂never␈α∞proved␈α∞correct␈α∞-␈α∂either␈α∞by
␈↓ ↓H␈↓hand␈α∂or␈α∂machine.␈α∞ It␈α∂is␈α∂disgraceful␈α∞that␈α∂the␈α∂referees␈α∞wrote␈α∂their␈α∂own␈α∞program.␈α∂ It␈α∂is␈α∂almost␈α∞as
␈↓ ↓H␈↓though␈α∂a␈α∞proof␈α∂was␈α∞o≥ered␈α∂that␈α∞consisted␈α∂of␈α∞a␈α∂selection␈α∞of␈α∂cases␈α∞and␈α∂the␈α∞referees␈α∂accepted␈α∞the
␈↓ ↓H␈↓paper on the basis of some further examples.

␈↓ ↓H␈↓        Whether␈α∞one␈α∞regards␈α∞the␈α∞above␈α∞analogy␈α∞as␈α∂valid␈α∞or␈α∞not,␈α∞it␈α∞is␈α∞clear␈α∞that␈α∞assurance␈α∂of␈α∞the
␈↓ ↓H␈↓correctness␈αof␈αthe␈αfour␈αcolor␈αconjecture␈αwould␈αbe␈αgreater␈αif␈αthe␈αprogram␈αhad␈αbeen␈αproved␈αto␈αmeet
␈↓ ↓H␈↓certain␈α∂speci≡cations.␈α∂ Even␈α∂suppose␈α∂that␈α∂no-one␈α∂had␈α∂proved␈α∂anything␈α∂aobut␈α∂the␈α∞programming
␈↓ ↓H␈↓language,␈αthe␈αcompiler␈αor␈αthe␈αcomputer␈αitself.␈α
 It␈αis␈αultimately␈αdesirable␈αto␈αprove␈αthem␈αcorrect␈α
also,
␈↓ ↓H␈↓but␈αthere␈α
is␈αan␈α
important␈αdistinction␈α
between␈αthem␈α
and␈αthe␈α
program␈αspeci≡cally␈α
intended␈αto␈α
verify
␈↓ ↓H␈↓the␈α∂conjecture␈α∂in␈α∞that␈α∂the␈α∂latter␈α∞is␈α∂subject␈α∂to␈α∂wishful␈α∞thinking␈α∂by␈α∂the␈α∞author␈α∂and␈α∂even␈α∂by␈α∞the
␈↓ ↓H␈↓referees.

␈↓ ↓H␈↓        My␈αsuggestion␈αthen␈αis␈αthat␈αthe␈αcommittee␈αo≥er␈αa␈αprize␈αfor␈αthe␈α≡rst␈αcomputer-checked␈αproof
␈↓ ↓H␈↓(whether␈αgenerated␈αby␈α
computer␈αor␈αnot)␈α
that␈αa␈αprogram␈αis␈α
correct␈αthat␈αis␈α
the␈αbasis␈αof␈αa␈α
substantial
␈↓ ↓H␈↓published proof of a matematical conjecture.

␈↓ ↓H␈↓        There␈α⊃is␈α∩a␈α⊃lesser␈α∩example␈α⊃than␈α∩the␈α⊃four␈α⊃color␈α∩theorem␈α⊃which␈α∩I␈α⊃understand␈α∩better.␈α⊃ A
␈↓ ↓H␈↓Stanford␈α
CS␈αgraduate␈α
student␈αnamed␈α
Oren␈αPatashnik,␈α
while␈αat␈α
Yale,␈αproved␈α
that␈α
3␈αdimensional
␈↓ ↓H␈↓tic-tac-toe␈α∞with␈α
four␈α∞on␈α
a␈α∞side␈α
is␈α∞a␈α∞win␈α
for␈α∞the␈α
≡rst␈α∞player␈α
using␈α∞about␈α
1500␈α∞hours␈α∞of␈α
computer
␈↓ ↓H␈↓time.␈α∞ The␈α∞paper␈α∞about␈α∂it␈α∞was␈α∞recently␈α∞published␈α∞in␈α∂␈↓↓Mathematics␈α∞Magazine␈↓.␈α∞ In␈α∞my␈α∂opinion,␈α∞it
␈↓ ↓H␈↓wouldn't be very hard to prove correct a program that veri≡es cases.
␈↓ ↓H␈↓αProfessor W. W. Bledsoe␈↓ ¬ODecember 22, 1980␈↓ 
nPage 2␈↓ 


␈↓ ↓H␈↓        Like␈α
the␈α∞four␈α
color␈α∞problem,␈α
Patashniks␈α
proof␈α∞involved␈α
≡nding␈α∞winning␈α
moves␈α∞in␈α
certain
␈↓ ↓H␈↓situations␈α
with␈α∞the␈α
help␈α∞of␈α
the␈α∞computer␈α
and␈α
then␈α∞using␈α
the␈α∞computer␈α
to␈α∞verify␈α
that␈α∞the␈α
moves
␈↓ ↓H␈↓were␈α
winning␈α
and␈α
the␈α
positions␈α
formed␈α
an␈α
adequate␈α
set.␈α
 I␈α
think␈α
he␈α
or␈α
someone␈α
else␈α
would␈α
deserve
␈↓ ↓H␈↓a␈α⊂moderate␈α⊂prize␈α⊂for␈α⊂a␈α⊂computer␈α⊂checked␈α∂proof.␈α⊂ More␈α⊂than␈α⊂likely,␈α⊂a␈α⊂new␈α⊂program␈α⊂would␈α∂be
␈↓ ↓H␈↓written␈α⊃for␈α⊃the␈α∩veri≡cation␈α⊃work␈α⊃that␈α⊃would␈α∩be␈α⊃easier␈α⊃to␈α⊃prove␈α∩correct␈α⊃and␈α⊃would␈α⊃run␈α∩in␈α⊃a
␈↓ ↓H␈↓reasonable time.


␈↓ ↓H␈↓Best regards,



␈↓ ↓H␈↓John McCarthy
␈↓ ↓H␈↓Professor of Computer Science